#ifndef EVAL_HH_
# define EVAL_HH_

///
/// \file eval.hh
/// \brief Definition of the Evaluation function..
/// \author Coddy Levi, Sylvain Lobry
/// \version 1.0
///
/// Definition of the function that evaluates a formula.
///

# include "CTLLexer.hh"
# include "CTLParser.hh"
# include "Model.hh"
# include "basic_set_operations.hh"

# include <bdd.h>

///
/// \exception UnknownVariableException variable doesn't exist
///
class UnknownVariableException: public std::exception
{
public:
  UnknownVariableException(std::string& varname)
  {
    this->varname = varname;
  }

  virtual const char* what() const throw()
  {
    std::string msg = std::string("Unknown Variable \"") + varname + "\"";

    return msg.c_str();
  }

  virtual ~UnknownVariableException() throw()
  {
  }

private:
  std::string varname;
};

///
/// \fn bdd eval (AST* formula, Model& model)
/// \brief The main function of evaluation of a formula.
///
/// \param[in]		formula The formula to be evaluated.
/// \param[in]		model The model that represents the Kripke structure.
///
/// \return		The resulting bdd.
///
bdd
eval (AST*	formula,
      Model&	model);

#endif /* !EVAL_HH_ */
